% ----- base functions --------------------------------------------------------

conlist([],""):-!.
conlist([Str],Str):-!.
conlist([Str1,Str2],Res):-
	concat(Str1,Str2,Res),!.
conlist([H|T],Res):-
	conlist(T,Temp),
	concat(H,Temp,Res).
	
list_commastr([],'') :- !.
list_commastr([S],S) :- !.
list_commastr([S1|L], S) :-
  list_commastr(L,S2),
  conlist([S1, ', ', S2], S).

printt((A,B)) :- !, print('('), printt(A), print(','), printt(B), print(')').
printt(X) :- print(X).

% ----- string representation of atoms etc. -----------------------------------

% e.g. S1='pi_'
stringrepr(S, (A,2)) :- stringrepr(S1,A), conlist(['{',S1,'}\''],S), !.
stringrepr(S, (A,B)) :- stringrepr(S1,A), stringrepr(S2,B), conlist([S1,',',S2],S), !.
stringrepr(S, ss((A,B),C)) :- stringrepr(S1,A),stringrepr(S2,B),stringrepr(S3,C),conlist([S3,'[',S1,'_{',S2,'}]'],S), !.
stringrepr(S, ss(A,B)) :- stringrepr(S1,A),stringrepr(S2,B),conlist([S2,'[',S1,']'],S), !.
stringrepr('\\cdot', dot) :- !.
stringrepr(S, X) :- string_to_atom(S1, X), stringrepr2(S1, S).

% e.g. S1='pi_1_', S='\pi_{1}'
stringrepr2(S1, S) :- concat(S2,'_',S1), stringrepr2(S2,S3), concat('\\',S3,S), !.
stringrepr2(S1, S) :- concat(S2, S3, S1), concat('_', S4, S3), stringrepr3(S2,S22), stringrepr3(S4, S44), string_length(S4, L), L>1, conlist([S22,'_{',S44,'}'], S), !.
stringrepr2(S1, S) :- concat(S2, S3, S1), concat('_', S4, S3), stringrepr3(S2,S22), stringrepr3(S4, S44), string_length(S4, 1),      conlist([S22,'_{',S44,'}'], S), !.
stringrepr2(S1,S) :- stringrepr3(S1,S).

% e.g. S1='a_b', S='a,b'
% the following is hugely inelegant and inefficient, but hey, it seems to work..
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('_', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,',',S44], S), !.
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('I', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,'\'',S44], S), !.
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('P', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,'^+',S44], S), !.
stringrepr3(S1, S) :- concat(S2, S3, S1), concat('M', S4, S3), stringrepr3(S2, S22), stringrepr3(S4, S44), conlist([S22,'^-',S44], S), !.
stringrepr3(S,S).


% ----- context items --------------------------------------------------------------

% examine der files for isunique (when printing a state, which defines knows,
% we cannot load another state file for isunique, so we need to use the
% corresponding der file)
findm(M) :- current_predicate(der,2), der(_,M).
% examine knowledge for isunique
findm(M) :- knows(_,M).

isunique(_) :- false.

%isunique(ctxm(_,P,V,I,_)) :- 
%  findall(CTX,(CTX=ctxm(_,P,V,I2,_),findm(Y),contains(Y,CTX),I2\=I),ALLCTX1),
%  list_to_set(ALLCTX1,ALLCTX2),
%  length(ALLCTX2,L), L>0.

string_message(S, X) :- atom(X), stringrepr(S,X).
string_message(S,M) :-
  hasproperty2(ctxm(D,P,V,_,_),M,T), !, 
  stringrepr(SD,D), stringrepr(SP,P), stringrepr(SV,V), stringrepr(ST,T), 
  conlist(['\\attpredctx{', SV, '}{', SD, '}{', SP, '}{', ST, '}'], S).
%\newcommand{\attpredctx}[4]{\ctxm{{#1}?_{#4}}{#2}{#3}}

string_message(S, M) :-
  M=ctxm(D,P,V,_,_), isunique(M),
  stringrepr(SD, D), stringrepr(SP, P), stringrepr(SV, V),
  conlist(['\\ctxm{\\mathbf{', SV, '}}{', SD, '}{', SP, '}'], S).
string_message(S, M) :-
  M=ctxm(D,P,V,_,_), not(isunique(M)),
  stringrepr(SD, D), stringrepr(SP, P), stringrepr(SV, V),
  conlist(['\\ctxm{', SV, '}{', SD, '}{', SP, '}'], S).
% string_message(S, pri(lst,L)) :- % special short notation for message+signature
%   L=[M2,pri(s,[M1,M2])],
%   string_message(S1,M1), string_message(S2,M2),
%   conlist(['\\textrm{MS}_{',S1,'}(',S2,')'], S), !.

% ----- messages --------------------------------------------------------------

string_message(S, pri(lst,L)) :-
  findall(X,(member(I,L),string_message(X,I)),L2),
  list_commastr(L2,S1),
  conlist(['\\{',S1,'\\}'], S), !.

% standard messages
string_message(S, pri(T,L)) :-
  findall(X,(member(I,L),string_message(X,I)),L2),
  list_commastr(L2,S1),
  conlist(['\\mathsf{', T, '}(', S1, ')'], S).
  
stepstr(step(A,B,tm(_,[pri(naught,[]),pri(naught,[])],M)),STR) :- !,
  stringrepr(SA,A),
  stringrepr(SB,B),
  string_message(SM,M),
  conlist(['\\transalignn{',SA,'}{',SB,'}{',SM,'}'], STR).

stepstr(step(A,B,tm(_,[IDA,IDB],M)),STR) :-
  stringrepr(SA,A),
  stringrepr(SB,B),
  string_message(SIDA,IDA),
  string_message(SIDB,IDB),
  string_message(SM,M),
  conlist(['\\transalign{',SA,'}{',SIDA,'}{',SB,'}{',SIDB,'}{',SM,'}'], STR).

% ---- actors -----------------------------------------------------------------


printact0(A) :- atomic(A), detect([(_,s)],_), !, print(A), print('*').
printact0(A) :- atomic(A), print(A).
printact0((A,s)) :- print(A).

printact(A) :- current_predicate(printactor/1), !, printactor(A).
printact(A) :- printact0(A).

printacts(LST) :- print('['),printactsp(LST),print(']').
printactsp([]).
printactsp([X]) :- printact(X), !.
printactsp([X|LST]) :- printact(X),print(','),printactsp(LST).
